package simplytypeddebruijn

trait SimplyTypedDeBruijnSubstitution extends TermSubstitutionProvider {self: TermSubstitutionProvider with AbstractSyntax =>
  
  object DeBruijnOps {
    
    type Term = LTerm
    type Type = LType
    
    def termSubstTop(v: Term, t: Term): Term = {
      termShift(-1,
          	  termSubst(0,
                        termShift(1,v),
                        t))
                //debugging in eclipse: use verbose version
                //{val termsubst= termSubst(0, 
                //          {val valunderbinder = termShift(1,v);valunderbinder},
                //          t );termsubst} )
    }
    
    
    def termShift(d: Int, t: Term) = {
      termMap((c:Int,x:Var) => if (x.n >=c) Var(x.n+d) else Var(x.n) ,
              (c:Int,x:Type) => x, //typeShiftAbove(d,c,x) ,
              0,t) //initial cutoff is 0
    }
    
    
    def termSubst(j: Int, s: Term,t: Term) = {
      termMap((c:Int,x:Var) => if (x.n == j+c) termShift(c,s) else Var(x.n),
              (c:Int,x:Type) => x,
              j,t)
    }
    
    
    
    def termMap(onvar:(Int,Var)=>Term, ontype:(Int,Type)=>Type, i:Int, t:Term) ={

         
      def walk(c: Int, t: Term) : Term = t match {
        case Var(nb)        => onvar(c,Var(nb))
        case Lam(x,ty,t1)   => Lam(x,ontype(c,ty),walk(c+1,t1)) //+1 because we are looking inside a new scope
        case App(t1,t2)     => App(walk(c,t1),walk(c,t2))
        
        case Let(x,t1,t2) => Let(x,walk(c,t1), walk(c+1, t2))
        
        case Record(fields)=> {
          val fields_ = fields.map({case (label,fld) => (label, walk(c,fld))})
          Record(fields_)
        }
        case RecProj(r,label)  => RecProj(walk(c,r),label)
        
        case base:BaseValue=> base
        case If(cond,p,n)  => If(walk(c,cond),walk(c,p),walk(c,n))  
      }
      walk(0,t)
    }
    
  }
  import DeBruijnOps._


  
  type partial = bruijnpart
  type topsubst = bruijntopsubst
  
  def substituteterm(v:Term)=new bruijnpart(v)
  class bruijnpart(v:Term) extends examplepartial(v) {
    def asTop() = new bruijntopsubst(v)
  }
  class bruijntopsubst(v:Term) extends exampletopsubst(v) {
    def intoterm(term: Term)= (v,term) match {
      case (v:Term,t:Term)  => termSubstTop(v,t)
    }
  }
    

}



